pnueli-zuck.10.jani:model: info: pnueli-zuck.10 is an MDP model and will be simulated as an MDP.
pnueli-zuck.10.jani:variables[0]: info: Expanding variable "p0" into 16 locations in automaton "process0".
pnueli-zuck.10.jani:variables[1]: info: Expanding variable "p1" into 16 locations in automaton "process1".
pnueli-zuck.10.jani:variables[2]: info: Expanding variable "p2" into 16 locations in automaton "process2".
pnueli-zuck.10.jani:variables[3]: info: Expanding variable "p3" into 16 locations in automaton "process3".
pnueli-zuck.10.jani:variables[4]: info: Expanding variable "p4" into 16 locations in automaton "process4".
pnueli-zuck.10.jani:variables[5]: info: Expanding variable "p5" into 16 locations in automaton "process5".
pnueli-zuck.10.jani:variables[6]: info: Expanding variable "p6" into 16 locations in automaton "process6".
pnueli-zuck.10.jani:variables[7]: info: Expanding variable "p7" into 16 locations in automaton "process7".
pnueli-zuck.10.jani:variables[8]: info: Expanding variable "p8" into 16 locations in automaton "process8".
pnueli-zuck.10.jani:variables[9]: info: Expanding variable "p9" into 16 locations in automaton "process9".
pnueli-zuck.10.jani: info: Using default value of 0.95 for the confidence parameter.
Peak memory usage: 324 MB
Analysis results for pnueli-zuck.10.jani
Status: Finished
Simulation time: 335.3 s
+ Property Property "live"
Estimated max. probability: 1
Runs used (best scheduler): 250
Total runs used: 35521650
Schedulers sampled: 35000
Best scheduler: 164617082
Run type: MDP
Status: Finished
+ Error bounds
Scheduler sampling: The result is a lower bound for the true max. probability.
Statement: Adaptive: P(error > εp̂) < δ
ε: 0.02
δ: 0.050000000000000044